(A ^ B) FALSE, while A and B are TRUE?

32 views
Skip to first unread message

Pierre Haessig

unread,
May 27, 2025, 1:58:45 PM (6 days ago) May 27
to MiniZinc
Hello,

I'm facing a strange result with the attached Minizinc model (using Minizing IDE 2.9.3 on Linux). It contains piecewise linear expressions (a mixture of floats and bools, in the spirit of my previous message).

It is quite long, but it contains the following constraints:

constraint gen_ok = (gen_ok1 /\ gen_ok2);
constraint op = gen_ok /\ ....
constraint ... /\ not op;
solve satisfy;

When solved with HiGHS, I get the UNSATISFIABLE status, which I believe is the correct answer.

However, if I solve with Gecode, not only do I get a satisfiable result, but also I get the following strange result:

gen_ok=false ....
gen_ok1=true  gen_ok2=true

which is pretty strange, since it boils down to (A ^ B) FALSE, while A and B are TRUE...

Did I make a syntax error?

Thanks for your feedback.

Best,
Pierre
Dispatch_verification.mzn

krzysztof....@gmail.com

unread,
May 27, 2025, 6:19:31 PM (5 days ago) May 27
to MiniZinc
Just put parentesisi for 

constraint op = gen_ok /\ ....

so it will be 

constraint op = (gen_ok /\ ....)

Best,
/Kris

Pierre Haessig

unread,
May 28, 2025, 6:31:03 PM (4 days ago) May 28
to MiniZinc
Thanks for the feedback. I had spent some time studying operator precedence at https://docs.minizinc.dev/en/stable/spec.html#operators, but still I had missed that one. I guess I still have some "imperative language" bias where "=" stands for assignment.

Now, having fixed this I wonder if I still have some syntax error, or if I'm just facing a solving tolerance issue.

Here is the result of running  the updated code:

  • Gecode: doesn't converge after some seconds
  • COIN-BC: UNSATISFIABLE (which I expect to be the true result)
  • HiGHS: returns the following satisfiable result, which is really at the edge of the constraints

nl=100.0
gen=-2.524757246869761e-15  gen_max=0.0
batt=100.0  batt_min=-0.0 batt_max=100.0
shed=-2.524757246869761e-15  spill=-2.524757246869761e-15
Decision tree: dt=true  dtcase=DT_maxbatt
nl_neg=false  nl_l_batt_min=false  nl_le_batt_max=true  nlmbatt_le_gen_max=true
Operating constraints: op=false
gen_ok=true  batt_ok=true  shed_ok=true  spill_ok=true  balance_ok=false (deltaP=0.0)

In particular, the odd result is at the end

balance_ok=false (deltaP=0.0)

where the relevant variables and constraints are:

set of float: bfloat = -100.0..100.0;
var bfloat: deltaP = gen+batt-spill - (nl-shed); % generation - load, including spillage and load shedding
var bool: balance_ok;
constraint balance_ok = (deltaP == 0.0);

Best,
Pierre
Dispatch_verification.mzn

krzysztof....@gmail.com

unread,
May 29, 2025, 12:42:57 PM (4 days ago) May 29
to MiniZinc
I have got the following result from Gecode (JaCoP result is similar). 

nl=-99.9999999999999

gen=-0.0 gen_max=0.0

batt=-99.9999999999999 batt_min=-99.9999999999999 batt_max=0.0

shed=-0.0 spill=-1.4210854715202e-14

Decision tree: dt=false dtcase=DT_spill

nl_neg=true nl_l_batt_min=false nl_le_batt_max=true nlmbatt_le_gen_max=true

Operating constraints: op=false

gen_ok=true batt_ok=false shed_ok=true spill_ok=false balance_ok=false (deltaP=1.4210854715202e-14)

----------


I guess this is due to rounding errors in floating-point numbers :( It has been pointed out in several discussions on minizinc with floating-points and constraint solvers.


BTW, I used the following annotation for search.


solve :: float_search([nl, gen, gen_max, batt, batt_min, batt_max, shed, spill],
                      1e-16, most_constrained, indomain_split) satisfy;


Reply all
Reply to author
Forward
0 new messages